package ai.子句集;

import java.util.*;
import java.util.regex.Matcher;
import java.util.regex.Pattern;

public class 子句集 {

    private String s;

    private Map<Integer, String> sMap;

    子句集(String s) {
        this.s = s;
        this.sMap = new HashMap<>();
        sMap.put(0, s);
    }

    public static void main(String[] args) {
        子句集 z = new 子句集("∀x(∀yP(x,y)->~∀y(Q(x,y)->R(x,y)))");
        z.init();
    }

    //∀ ∃ ∧ ∨ ～ -> <-->
    //∀x(∀yP(x,y)->~∀y(Q(x,y)->R(x,y)))
    //首先要做的是匹配括号
    private void init() {
        toSplit(s);

        System.out.println(Arrays.toString(sMap.entrySet().toArray()));

        removeEqual();

        System.out.println(Arrays.toString(sMap.entrySet().toArray()));

        reduceScope();

        System.out.println(Arrays.toString(sMap.entrySet().toArray()));
    }

    /**
     * 根据括号分割
     * @param s
     */
    private void toSplit(String s) {
        char[] chars = s.toCharArray();

        //字符串分割开始和结束位置
        int start = -1,end;
        int count = 0;
        for (int i = 0; i < chars.length; i++) {
            if (-1 == start) {
                if ('(' == chars[i]) {
                    start = i;
                    count++;
                }
            } else {
                if ('(' == chars[i]) {
                    count++;
                } else if (')' == chars[i]) {
                    count--;
                }

                if (0 == count) {
                    end = i;

                    String newS = s.substring(start + 1, end);
                    sMap.put(sMap.size(), newS);

//                    //因为刚刚又添加了一个，所以就要减2啊...
//                    sMap.put(sMap.size() - 2, sMap.get(sMap.size() - 2).replace(newS, String.valueOf(sMap.size() - 1)));

                    if (newS.contains("(")) {
                        toSplit(newS);
                    }

                    start =  -1;
                }
            }
        }
    }

    /**
     * 消除蕴含式和等值式
     */
    private void removeEqual(){
        for (int i = sMap.size() - 1; i >= 0; i--) {
            //如果该式子含有蕴含式
            if (sMap.get(i).contains("->")) {
                String[] temps = sMap.get(i).split("->");
                String newTemp = "~" + temps[0] + "∨" + temps[1];
                for (int j = 0; j <= i; j++) {
                    //如果含有刚刚的蕴含式，则进行替换
                    if (sMap.get(j).contains(sMap.get(i))) {
                        sMap.put(j, sMap.get(j).replace(sMap.get(i), newTemp));
                    }
                }
            }
            //如果该式子含有等值式
            else if (sMap.get(i).contains("<-->")) {
                String[] temps = sMap.get(i).split("<-->");
                String newTemp = "(~" + temps[0] + "∨" + temps[1] + ")∧(~" + temps[1] + "∨" + temps[0] + ")";
                for (int j = 0; j <= i; j++) {
                    //如果含有刚刚的蕴含式，则进行替换
                    if (sMap.get(j).contains(sMap.get(i))) {
                        sMap.put(j, sMap.get(j).replace(sMap.get(i), newTemp));
                    }
                }
            }
        }
    }

    /**
     * 缩小否定词的作用范围
     */
    private void reduceScope() {
        for (int i = 0; i < sMap.size(); i++) {
            for (int j = i+1; j < sMap.size(); j++) {
                if (sMap.get(i).contains(sMap.get(j))) {
                    //转换成一个尽量不被里面所打扰的串
                    String tempNum = String.valueOf(j);
                    String temp = sMap.get(i).replace(sMap.get(j), tempNum);
                    //如果替换完的仍然有非，则进行判断
                    if (temp.contains("~")) {
                        temp = temp.replace(tempNum, sMap.get(Integer.parseInt(tempNum)));
                        //~(~A) -> A
                        if (temp.contains("~(~")) {
                            temp = temp.replace("~(~", "").substring(0, temp.length() - 1);
                        }
                        //~(A and B) -> ~A or ~B
                        Pattern pattern0 = Pattern.compile("~\\((.*)∧(.*)\\)");
                        Matcher matcher0 = pattern0.matcher(temp);
                        if (matcher0.find()) {
                            String[] inString = sMap.get(j).split("∧");
                            temp = "~" + inString[0] + "∨~" + inString[1];
                        }
                        //~(A and B) -> ~A or ~B
                        Pattern pattern1 = Pattern.compile("~\\((.*)∨(.*)\\)");
                        Matcher matcher1 = pattern1.matcher(temp);
                        if (matcher1.find()) {
                            String[] inString = sMap.get(j).split("∨");
                            temp = "~" + inString[0] + "∧~" + inString[1];
                        }
                        //~all x P(x) -> exist x ~P(x)
                        if (temp.contains("~∀")) {
                            StringBuilder newJ = new StringBuilder();
                            String[] newJArrayTemp = sMap.get(i).split("~∀");
                            for (String newJTemp : newJArrayTemp) {
                                newJ.append("∃").append(newJTemp.charAt(0)).append("~").append(newJTemp.substring(1));
                            }
                            temp = newJ.toString();
                        }

                        //~exist x P(x) -> all x ~P(x)
                        if (temp.contains("~∃")) {
                            temp = temp.replace("~∃", "∀").replace(sMap.get(j), "~" + sMap.get(j));
                        }
                        sMap.put(i, temp);
                    }
                    break;
                }
            }
        }
    }
}
